摘要 :
Runtime monitoring is generally considered a light-weight alternative to formal verification. In safety-critical systems, however, the monitor itself is a critical component. For example, if the monitor is responsible for initiati...
展开
Runtime monitoring is generally considered a light-weight alternative to formal verification. In safety-critical systems, however, the monitor itself is a critical component. For example, if the monitor is responsible for initiating emergency protocols, as proposed in a recent aviation standard, then the safety of the entire system critically depends on guarantees of the correctness of the monitor. In this paper, we present a verification extension to the Lola monitoring language that integrates the efficient specification of the monitor with Hoare-style annotations that guarantee the correctness of the monitor specification. We add two new operators, assume and assert, which specify assumptions of the monitor and expectations on its output, respectively. The validity of the annotations is established by an integrated SMT solver. We report on experience in applying the approach to specifications from the avionics domain, where the annotation with assumptions and assertions has lead to the discovery of safety-critical errors in the specifications. The errors range from incorrect default values in offset computations to complex algorithmic errors that result in unexpected temporal patterns.
收起
摘要 :
Runtime monitoring is generally considered a light-weight alternative to formal verification. In safety-critical systems, however, the monitor itself is a critical component. For example, if the monitor is responsible for initiati...
展开
Runtime monitoring is generally considered a light-weight alternative to formal verification. In safety-critical systems, however, the monitor itself is a critical component. For example, if the monitor is responsible for initiating emergency protocols, as proposed in a recent aviation standard, then the safety of the entire system critically depends on guarantees of the correctness of the monitor. In this paper, we present a verification extension to the Lola monitoring language that integrates the efficient specification of the monitor with Hoare-style annotations that guarantee the correctness of the monitor specification. We add two new operators, assume and assert, which specify assumptions of the monitor and expectations on its output, respectively. The validity of the annotations is established by an integrated SMT solver. We report on experience in applying the approach to specifications from the avionics domain, where the annotation with assumptions and assertions has lead to the discovery of safety-critical errors in the specifications. The errors range from incorrect default values in offset computations to complex algorithmic errors that result in unexpected temporal patterns.
收起
摘要 :
This paper presents a performance assessment of a method to generate trajectories for a small unmanned rotorcraft within an obstacle field using a standardized set of benchmark scenarios. The dynamics of the rotorcraft are discret...
展开
This paper presents a performance assessment of a method to generate trajectories for a small unmanned rotorcraft within an obstacle field using a standardized set of benchmark scenarios. The dynamics of the rotorcraft are discretized into a set of motion primitives. For the generation of these primitives a formulation of a path-tracking optimal control problem is used. This optimal control problem has been previously shown to achieve trajectories that can be flown very accurately in flight tests. The generated primitives are used to convert the original task within the obstacle field into a discretized planning problem using sequential decision making that is solved using an optimal graph search algorithm (e.g., Dijkstra). This algorithm selects from and combines the available motion primitives to achieve the transition between a start and a goal waypoint in minimum time. We present results of this planning approach and include a scaling analysis for simple artificial as well as more complex urban environments.
收起
摘要 :
This paper presents a performance assessment of a method to generate trajectories for a small unmanned rotorcraft within an obstacle field using a standardized set of benchmark scenarios. The dynamics of the rotorcraft are discret...
展开
This paper presents a performance assessment of a method to generate trajectories for a small unmanned rotorcraft within an obstacle field using a standardized set of benchmark scenarios. The dynamics of the rotorcraft are discretized into a set of motion primitives. For the generation of these primitives a formulation of a path-tracking optimal control problem is used. This optimal control problem has been previously shown to achieve trajectories that can be flown very accurately in flight tests. The generated primitives are used to convert the original task within the obstacle field into a discretized planning problem using sequential decision making that is solved using an optimal graph search algorithm (e.g., Dijkstra). This algorithm selects from and combines the available motion primitives to achieve the transition between a start and a goal waypoint in minimum time. We present results of this planning approach and include a scaling analysis for simple artificial as well as more complex urban environments.
收起
摘要 :
Machine learning has proven to be the tool of choice for achieving human-like or even super-human performance with automation on specific tasks. As a result, this data-driven approach is currently experiencing massive interest in ...
展开
Machine learning has proven to be the tool of choice for achieving human-like or even super-human performance with automation on specific tasks. As a result, this data-driven approach is currently experiencing massive interest in all industry domains. This increased use also applies for the safety critical aviation domain. With no human pilot on board, the potential use cases of machine learning for unmanned aircraft are particularly promising. Even upcoming Urban Air Mobility concepts are planning to remove the onboard pilot and instead use machine learning to support a remote pilot, possibly supervising a fleet of vehicles. However, the verification of machine learning algorithms is a challenging problem, since established safety standards and assurance methods are not applicable. Thus, this work comprises a literature study on the topic of machine learning verification and safety. This research paper uses a systematic approach to map and categorize the research and focuses on specific subtopics that are of particular interest in the context of existing guidance documents.
收起
摘要 :
Naval aviators use tethers to assist rotorcraft during ship board landing because of the ability to increase robustness against wind turbulence and to center the rotorcraft on the landing spot. Autonomous tethered landing with unm...
展开
Naval aviators use tethers to assist rotorcraft during ship board landing because of the ability to increase robustness against wind turbulence and to center the rotorcraft on the landing spot. Autonomous tethered landing with unmanned rotorcraft and automatic winch device for applying the tether force requires the knowledge of how the tether force impacts the wind affected dynamics of the rotorcraft. To this day, the influences of applied tether force and wind velocity on robustness and stability of the rotorcraft have been little explored. In this paper, we present an analysis of the dynamics and stability of a nonlinear model of a small-scale tethered rotorcraft. We develop a simplified model of a rotorcraft's longitudinal dynamics and vary model parameters including tether force, trim conditions, and the horizontal wind in order to study the interdependence of those parameters and their impact on the model's equilibrium points and stability. This is a preliminary step towards design of an automatic control of an unmanned rotorcraft capable of autonomous tethered landing and development of tether force control laws for the winch device.
收起
摘要 :
The introduction of machine learning in the aviation domain is an ongoing process. This is also true for safety-critical domains, especially for the area of Urban Air Mobility. A significant growth in number of air taxis and an in...
展开
The introduction of machine learning in the aviation domain is an ongoing process. This is also true for safety-critical domains, especially for the area of Urban Air Mobility. A significant growth in number of air taxis and an increasing level of autonomy is to be expected allowing for operating a large number of air taxis in complex urban environments. Due to the complexity of the tasks and the environment, key autonomy functions will be realized using machine learning, for example the camera-based detection of objects. However, the safety assurance for avionics systems using machine learning components is challenging. This work investigates safety and verification aspects of machine learning components. A camera-based detection of humans on the ground, e.g. to assess a potential landing area, serves as an example for an machine learning-based autonomy functio and was integrated into an Unmanned Aircraft. In the context of this exemplary machine learning component, the concept of Operational Design Domain as recently adapted European Aviation Safety Agency in the context of machine learning assurance is described along with other key concepts of machine learning assurance. Furthermore, runtime assurance is used to monitor conformance to the Operational Design Domain during flight. The presented flight test results indicate that monitoring the Operational Design Domain can support performance as well as the safety of the operation.
收起
摘要 :
Monitoring capabilities play a central role in mitigating safety risks of current, and especially future autonomous aircraft systems. These future systems are likely to include complex components such as neural networks for enviro...
展开
Monitoring capabilities play a central role in mitigating safety risks of current, and especially future autonomous aircraft systems. These future systems are likely to include complex components such as neural networks for environment perception, which pose a challenge for current verification approaches; they are considered as black-box components. To assure that these black-boxes comply with their specification, they must be monitored to detect violations during execution with respect to their input and output behaviors. Such behavioral properties often include more complex aspects such as temporal or spatial notions. The outputs can also be compared to data from other assured sensors or components of the aircraft, making monitoring an integral part of the system, which ideally has access to all available resources to assess the overall health of the operation. Current approaches using handwritten code for monitoring functions run the risk of not being able to keep up with these challenges. Therefore, in this paper, we present a hierarchy of monitoring properties that provides a perspective for overall health. We also present a categorization of monitoring properties and show how different monitoring specification languages can be used for formalization. These monitoring languages represent a higher abstraction of general-purpose code and are therefore more compact and easier for a user to write and read, and we can validate their implementations independently from the systems they reason about. They improve the maintainability of monitoring properties that is required to handle the increased complexity of future autonomous aircraft systems.
收起
摘要 :
HorizonUAM is a DLR project to research the vision of urban air mobility. One important topic is the safety and security aspect. This paper discusses the safety and security considerations in the topic areas of: safe autonomy, rel...
展开
HorizonUAM is a DLR project to research the vision of urban air mobility. One important topic is the safety and security aspect. This paper discusses the safety and security considerations in the topic areas of: safe autonomy, reliable multisensor navigation, robust and efficient communication, U-space and safe air traffic, and finally cyber-physical safety and security. As a basis for future discussion, the challenges and gaps are identified, furthermore the research in the context of the project is briefly outlined. From a safety perspective, the missing pilot of an autonomous vehicle is equivalent to a missing fallback layer, which has to be mitigated. Additionally, trust needs to be established for new techniques, specifically machine learning, which has recently gained massive interest. To solve this, verification, standardization, and regulation aspects of autonomy have to be addressed. The research is therefore targeted towards assessing and increasing the safety of autonomous operations. Moreover, a multi-sensor navigation system is necessary to achieve required safety levels in challenging environments, while meeting the cost and weight constraints. In order to ensure the integrity of the navigation system, an innovative integrity monitoring architecture for the multi-sensor solution will be investigated in the UAM context. Furthermore, many flying vehicles will need to share information in a reliable and trustworthy manner. Therefore, a robust and efficient communication system is specifically designed to meet the requirements of the future urban air mobility in order to mitigate midair collisions. To achieve safe air traffic, U-space services would have to be established. The project will specifically address gaps in the proposed services and identify additional required information and services. As a last aspect, the cyber physical safety and security has to be considered. With highly connected systems, attacks can happen over the Internet from virtually anywhere. Therefore, it is required to establish a holistic approach for cyber-physical safety and security.
收起
摘要 :
This paper considers the formation flight in the context of an automated aerial refueling mission of small-scale aircraft. The attention is concentrated on a simulation-based robustness analysis approach allowing fast re-evaluatio...
展开
This paper considers the formation flight in the context of an automated aerial refueling mission of small-scale aircraft. The attention is concentrated on a simulation-based robustness analysis approach allowing fast re-evaluation of a guidance algorithm, which steers the follower aircraft during the formation flight. The simulation, on which this robustness analysis is based, is easily extendable in order to include gained insight of future experiments. The paper presents results obtained from an exemplarily application of the robustness analysis to a preliminary guidance algorithm of a small unmanned aircraft. The application at this point includes a 3-degree-of-freedom leader aircraft model following an oval racetrack path and a 6-degree-of-freedom follower aircraft model, which is under the effect of wind.
收起
原文获取